  (   ∀(natural : Type)
    → ∀(succ : natural → natural)
    → ∀(zero : natural)
    → natural
  )
→ Natural
